Section: Software

Ssreflect

Participants : Assia Mahboubi [Contact] , Enrico Tassi.

SSReflect is a proof language extension of Coq developed under Georges Gonthier (Microsoft Research). It was originally designed to make the formalization of the Four Color Theorem possible and has been evolving since. It is important to note that it is shipped with redesigned basic proof libraries. Members of the Typical are in charge of the documentation and distribution of this extension.